#ifndef UTILITIES_HH
# define UTILITIES_HH
#include <vector>
#include <cmath>
#include "types.hh"
#include "cuddObj.hh"

using namespace std;

extern "C++"
{
    inline int log_2(int x)
    {
        if (x == 1)
            return 1;
        else
            return (int) ceil(log2(x));
    }
    BDD xorlist(vector<BDD> *bddlist);
    BDD Exists(BDDvector* v, BDD x);
    ADD ADDExists(ADDvector v, ADD x);
    BDD check_EX(BDD next);
    BDD check_EF(BDD p);
    BDD check_EG(BDD p);
    BDD check_EU(BDD p, BDD q);
    BDD check_AU(BDD p, BDD q);
    BDD check_nK(BDD next, BDD RK);
    BDD check_nO(BDD next, BDD RO);
    BDD check_nKH(BDD next, BDD RK, BDD RO);
    BDD check_GK(BDD next, BDD RK);
    BDD check_nGK(BDD next, BDD RK);
    BDD check_DK(BDD next, BDD RK);
    BDD check_nDK(BDD next, BDD RK);
    BDD check_GCK(BDD next, BDD RK);
    BDD check_GCK_new(BDD next, string name);
    BDD check_nDKH(BDD next, BDD RK, BDD RO);
    BDD check_ATLX(BDD next, string grpname);
    BDD check_ATLG(BDD p, string grpname);
    BDD check_ATLU(BDD q1, BDD q2, string grpname);

    BDD check_EG_fair(BDD p);
    BDD check_EF_fair(BDD p, BDD fair_reach);
    BDD check_EX_fair(BDD p, BDD fair_reach);
    BDD check_EU_fair(BDD p, BDD q, BDD fair_reach);
    BDD check_nK_fair(BDD next, BDD RK, BDD fair_reach);
    BDD check_nO_fair(BDD next, BDD RO, BDD fair_reach);
    BDD check_nKH_fair(BDD next, BDD RK, BDD RO, BDD fair_reach);
    BDD check_GK_fair(BDD next, BDD RK, BDD fair_reach);
    BDD check_nGK_fair(BDD next, BDD RK, BDD fair_reach);
    BDD check_DK_fair(BDD next, BDD RK, BDD fair_reach);
    BDD check_nDK_fair(BDD next, BDD RK, BDD fair_reach);
    BDD check_GCK_fair(BDD next, BDD RK, BDD fair_reach);
    BDD check_nDKH_fair(BDD next, BDD RK, BDD RO, BDD fair_reach);

    BDD get_K_states(BDD aset1, BDD *state, string name);
    BDD get_nK_states(BDD *state, string name);
    BDD get_nK_states_fair(BDD *state, string name, BDD fair_reach);
    BDD get_GK_states(BDD aset1, BDD *state, string name);
    BDD get_DK_states(BDD aset1, BDD *state, string name);
    BDD get_agent_greenstates(BDD aset1, string name);
    BDD get_group_greenstates(BDD aset1, string name);

    DdNode * addApplyLT(DdManager* mgr, DdNode ** n1, DdNode ** n2);
    DdNode * addApplyLE(DdManager* mgr, DdNode ** n1, DdNode ** n2);
    DdNode * addApplyGT(DdManager* mgr, DdNode ** n1, DdNode ** n2);
    DdNode * addApplyGE(DdManager* mgr, DdNode ** n1, DdNode ** n2);
    DdNode * addApplyEQ(DdManager* mgr, DdNode ** n1, DdNode ** n2);
    DdNode * addApplyNEQ(DdManager* mgr, DdNode ** n1, DdNode ** n2);

    ADD addLT(ADD a1, ADD a2);
    ADD addLE(ADD a1, ADD a2);
    ADD addGT(ADD a1, ADD a2);
    ADD addGE(ADD a1, ADD a2);
    ADD addEQ(ADD a1, ADD a2);
    ADD addNEQ(ADD a1, ADD a2);

    // Calculate X * RT with local transition relations
    BDD timesTrans(BDD *from, BDD *to);

    // Remove actions from X * RT
    BDD timesRT(BDD *state);

    BDD permuteBDDs(int start1, int start2, int length);
    BDD permuteAgents(int agent1, int agent2);
    BDD permuteAgents(string agentname1, string agentname2);
    string permutation_name(string prefix, map<string, string> *permutation);

    vector<map<string, string>*>* compute_round_permutation();
    vector<map<string, string>*>* compute_arbitrary_permutation();
}

extern map<string, int> options;
extern map<string, basic_agent *> *is_agents;
extern vector<basic_agent *> *agents;
extern map<string, bool_expression *> *is_evaluation;
extern bool_expression *is_istates;
extern map<string, set<string> > *is_groups;
extern vector<modal_formula> *is_formulae;
extern vector<fairness_expression *> *is_fairness;
extern int obsvars_bdd_length;
extern int envars_bdd_length;
extern Cudd *bddmgr;
extern BDDvector *v;
extern BDDvector *vRT;
extern ADDvector *addv;
extern BDDvector *pv;
extern ADDvector *addpv;
extern BDDvector *a;
extern BDD andprot;
extern BDD preRT;
extern BDD trans;
extern BDD RT;
extern BDD reach;
extern BDD reachRT;
extern map<string, BDD> er;
extern map<string, BDD> deor;
extern map<string, BDD> gm;
extern map<string, BDD> deogm;
extern map<string, BDD> distgm;
extern BDD fair_reach;
extern BDDvector *vevol;
extern BDDvector *vprot;
extern bool need_epistemic;
extern bool need_deontic;
extern bool need_common_knowledge;
extern bool need_deontic_knowledge;
extern bool need_distributed_knowledge;
extern bool calReachRT;
extern BDD in_st;
extern BDD* bddOne;
extern vector<vector<int> *> *countex; // For counterexamples
extern map<int, BDD *> *idbdd;
extern int scount;
extern vector<vector<transition *> *> *cextr;

extern map<string, BDD> *symmetry_cache;
extern map<string, string> *symmetry_atom_cache;

#endif // ! UTILITIES_HH
